Also, I broke several files down into more separate sections.

I'm a bit worried that these changes will make it considerably harder to get #1211 merged down the road. But since that PR has been stale for a while and there are likely other merged changes that already make this difficult I'm not sure it should be a blocker. I would be incredibly grateful if someone were to comb through that PR and try and get the more finished parts of it merged though, such as the well-ordering principle of the natural numbers and divisibility among many others.

I'm a bit worried that these changes will make it considerably harder to get #1211 merged down the road. But since that PR has been stale for a while and there are likely other merged changes that already make this difficult I'm not sure it should be a blocker. I would be incredibly grateful if someone were to comb through that PR and try and get the more finished parts of it merged though, such as the well-ordering principle of the natural numbers and divisibility among many others.

I'd like to get some feedback from another maintainer before this PR is potentially merged. Preferrably @EgbertRijke, but otherwise @VojtechStep, since I expect the former will not respond.

From what I've seen so far, this PR mostly abstracts definitions and fixes a few names. Are these changes necessary for your continued process @lowasser, or could we potentially icebox this PR until progress has been made to merge the other one? Otherwise, should we consider #1211 discontinued and not take it into consideration, @VojtechStep? Keep in mind I have not checked exactly how much overlap there are between these two PRs.

I don't think #1211 is becoming mergeable any time soon (it never typechecked, it's been stale for 8 months, and in any case a +17k-3k PR would be very hard to review in one go), and I don't think we should freeze elementary-number-theory until it's done. I'm sure it contains good ideas, and I hope the ideas should be rebasable onto this work, if not the actual code.

These are not necessary changes, just things that have irritated me.

I guess I'm just struggling to accept that #1211 is again not going to get merged, and this PR puts a final nail in its coffin. I'll okay these changes for merging.

It's worth emphasizing that the software practice I've been trained in, at least, emphasizes smaller PRs that try to do one thing. Not that this PR is a great example of that, but several separate changes, even ones with interdependencies, are easier to merge, less painful if they have to be dropped for whatever reason, faster to understand and review and make progress on...

I can see if I can try to rescue bits of it, though.